/-
Copyright (c) 2025 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/
module

public import Mathlib.Algebra.Module.Equiv.Defs
public import Mathlib.GroupTheory.Congruence.Basic

/-!
# Congruence relations respecting scalar multiplication
-/

@[expose] public section

variable (R S M N : Type*)

/-- A congruence relation that preserves additive action. -/
structure VAddCon [VAdd S M] extends Setoid M where
  /-- A `VAddCon` is closed under additive action. -/
  vadd (s : S) {x y} : r x y → r (s +ᵥ x) (s +ᵥ y)

/-- A congruence relation that preserves scalar multiplication. -/
@[to_additive] structure SMulCon [SMul S M] extends Setoid M where
  /-- A `SMulCon` is closed under scalar multiplication. -/
  smul (s : S) {x y} : r x y → r (s • x) (s • y)

/-- A congruence relation that preserves addition and scalar multiplication.
The quotient by a `ModuleCon` inherits `DistribSMul`, `DistribMulAction`, and `Module` instances. -/
structure ModuleCon [Add M] [SMul S M] extends AddCon M, SMulCon S M

/-- The `SMulCon` underlying an `ModuleCon`. -/
add_decl_doc ModuleCon.toSMulCon

variable {S}

namespace SMulCon

/-- The quotient by a congruence relation preserving scalar multiplication. -/
@[to_additive /-- The quotient by a congruence relation preserving additive action. -/]
protected def Quotient [SMul S M] (c : SMulCon S M) : Type _ := Quotient c.toSetoid

@[to_additive] instance [SMul S M] (c : SMulCon S M) : SMul S c.Quotient where
  smul s := Quotient.map (s • ·) (@c.smul s)

instance [SMul S M] [Zero M] (c : SMulCon S M) : Zero c.Quotient where
  zero := ⟦0⟧

instance [Zero M] [SMulZeroClass S M] (c : SMulCon S M) : SMulZeroClass S c.Quotient where
  smul_zero s := congr_arg _ (smul_zero s)

instance [Zero S] [Zero M] [SMulWithZero S M] (c : SMulCon S M) : SMulWithZero S c.Quotient :=
  fast_instance% Quotient.mk''_surjective.smulWithZero ⟨_, rfl⟩ fun _ _ ↦ rfl

@[to_additive] instance [Monoid S] [MulAction S M] (c : SMulCon S M) : MulAction S c.Quotient :=
  fast_instance% Quotient.mk''_surjective.mulAction (⟦·⟧) fun _ _ ↦ rfl

section addConGen

variable {M} [AddZeroClass M] [DistribSMul S M]

/-- The `AddCon` generated by a relation respecting scalar multiplication is a `ModuleCon`. -/
def addConGen' (r : M → M → Prop) (hr : ∀ (s : S) {m m'}, r m m' → r (s • m) (s • m')) :
    ModuleCon S M where
  toAddCon := addConGen r
  smul s _ _ h := ((addConGen r).comap (DistribSMul.toAddMonoidHom M s) <| by simp).addConGen_le
    (fun _ _ h ↦ .of _ _ (hr s h)) h

/-- The `AddCon` generated by a `SMulCon` is a `ModuleCon`. -/
protected abbrev addConGen (c : SMulCon S M) : ModuleCon S M := addConGen' c.r c.smul

end addConGen

end SMulCon

namespace ModuleCon

/-- The quotient by a congruence relation preserving addition and scalar multiplication. -/
protected def Quotient [Add M] [SMul S M] (c : ModuleCon S M) : Type _ := Quotient c.toSetoid

instance [SMul S M] [Add M] (c : ModuleCon S M) : SMul S c.Quotient :=
  inferInstanceAs (SMul S c.toSMulCon.Quotient)

instance [SMul S M] [Zero M] [Add M] (c : ModuleCon S M) : Zero c.Quotient where
  zero := ⟦0⟧

instance [SMul S M] [Add M] (c : ModuleCon S M) : Add c.Quotient :=
  inferInstanceAs (Add c.toAddCon.Quotient)

instance [SMul S M] [AddZeroClass M] (c : ModuleCon S M) : AddZeroClass c.Quotient :=
  inferInstanceAs (AddZeroClass c.toAddCon.Quotient)

instance [SMul S M] [AddCommMagma M] (c : ModuleCon S M) : AddCommMagma c.Quotient :=
  inferInstanceAs (AddCommMagma c.toAddCon.Quotient)

instance [SMul S M] [AddSemigroup M] (c : ModuleCon S M) : AddSemigroup c.Quotient :=
  inferInstanceAs (AddSemigroup c.toAddCon.Quotient)

instance [SMul S M] [AddCommSemigroup M] (c : ModuleCon S M) : AddCommSemigroup c.Quotient :=
  inferInstanceAs (AddCommSemigroup c.toAddCon.Quotient)

instance [SMul S M] [AddMonoid M] (c : ModuleCon S M) : AddMonoid c.Quotient :=
  inferInstanceAs (AddMonoid c.toAddCon.Quotient)

instance [SMul S M] [AddCommMonoid M] (c : ModuleCon S M) : AddCommMonoid c.Quotient :=
  inferInstanceAs (AddCommMonoid c.toAddCon.Quotient)

instance [SMul S M] [AddGroup M] (c : ModuleCon S M) : AddGroup c.Quotient :=
  inferInstanceAs (AddGroup c.toAddCon.Quotient)

instance [SMul S M] [AddCommGroup M] (c : ModuleCon S M) : AddCommGroup c.Quotient :=
  inferInstanceAs (AddCommGroup c.toAddCon.Quotient)

instance [Zero M] [Add M] [SMulZeroClass S M] (c : ModuleCon S M) : SMulZeroClass S c.Quotient :=
  inferInstanceAs (SMulZeroClass S c.toSMulCon.Quotient)

instance [Zero S] [Zero M] [Add M] [SMulWithZero S M] (c : ModuleCon S M) :
    SMulWithZero S c.Quotient :=
  inferInstanceAs (SMulWithZero S c.toSMulCon.Quotient)

instance [Monoid S] [Add M] [MulAction S M] (c : ModuleCon S M) : MulAction S c.Quotient :=
  inferInstanceAs (MulAction S c.toSMulCon.Quotient)

instance [AddZeroClass M] [DistribSMul S M] (c : ModuleCon S M) : DistribSMul S c.Quotient :=
  fast_instance% Quotient.mk''_surjective.distribSMul c.mk' fun _ _ ↦ rfl

instance [Monoid S] [AddMonoid M] [DistribMulAction S M] (c : ModuleCon S M) :
    DistribMulAction S c.Quotient := fast_instance%
  Quotient.mk''_surjective.distribMulAction c.mk' fun _ _ ↦ rfl

instance [Semiring S] [AddCommMonoid M] [Module S M] (c : ModuleCon S M) : Module S c.Quotient :=
  fast_instance% Quotient.mk''_surjective.module _ c.mk' fun _ _ ↦ rfl

end ModuleCon

section ker

variable {R M N}

/-- The kernel of a `MulActionHom` as a congruence relation. -/
@[to_additive /-- The kernel of an `AddActionHom` as a congruence relation. -/]
def SMulCon.ker [SMul R M] [SMul S N] {φ : R → S} (f : M →ₑ[φ] N) : SMulCon R M where
  __ := Setoid.ker f
  smul r _ _ h := by rw [Setoid.ker_def] at h ⊢; simp_rw [map_smulₛₗ, h]

/-- The kernel of a `DistribMulActionHom` as a congruence relation. -/
def ModuleCon.ker [Monoid R] [Monoid S] [AddMonoid M] [AddMonoid N] [DistribMulAction R M]
    [DistribMulAction S N] {φ : R →* S} (f : M →ₑ+[φ] N) : ModuleCon R M where
  __ := SMulCon.ker f.toMulActionHom
  __ := AddCon.ker f

/-- The first isomorphism theorem for semimodules in the case of a surjective homomorphism. -/
noncomputable def ModuleCon.quotientKerEquivOfSurjective [Semiring S] [AddCommMonoid M]
    [AddCommMonoid N] [Module S M] [Module S N] (f : M →ₗ[S] N) (hf : Function.Surjective f) :
    (ker f.toDistribMulActionHom).Quotient ≃ₗ[S] N where
  __ := AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf
  map_smul' s := by rintro ⟨⟩; apply map_smul f

end ker
